\documentclass[a4paper]{article}

\usepackage{listings}
\usepackage{color}
\usepackage{graphicx}
\usepackage{tikz}
\usepackage{multicol}

\usepackage[top=2.0cm, bottom=2.0cm, left=2.0cm, right=2.0cm]{geometry}

\begin{document}

\title{Embbeded Systems - Exercise 04}

\author{Antonios Motakis \and Jander Nascimento}

\maketitle

\section*{Model checking and fairness}

\subsection*{Question 01}

$
S_f=\nu Z.EX \land_{c \in C}(E Z \cup (Z \land C)) \newline
\quad = \nu Z.EX((E Z \cup ( Z \land c_1)) \land (E Z \cup (Z \land c_2))) \newline
\newline
Z_0=S \newline
Z_1=EX((E Z_0 \cup (Z_0 \land c_1) \land (E Z_0  \cup (Z_0 \land c_2)) \newline
\rightarrow EX((EF \{7\}) \land (EF\{4,9\})) \newline
\rightarrow EX(\{1-7\} \land \{1-5,8-9\}) \newline
\rightarrow EX(\{1-5\})=\{2-5\}
\newline
Z_2=EX((E Z_1 \cup (Z_1 \land c_1) \land (E Z_1  \cup (Z_0 \land c_2)) \newline
\rightarrow EX((E Z_1 \cup (Z_1 \land c_1) \land (E Z_1 \cup (Z_1 \land C_2))) \newline
\rightarrow EX((E\{2-5\} \cup \emptyset) \land (E \{2-5\} \cup \{4\})) \newline
\rightarrow EX(\emptyset \land (E \{2-5\} \cup \{4\})) = \emptyset \newline
Z_3=EX((E \emptyset \cup \emptyset) \land (E \emptyset \cup \emptyset))=\emptyset
$

So, in the given structure is \textbf{not} possible to find a fair path that obeys $c_1$ and $c_2$ contraints.

\subsection*{Question 02}

$
S_F=\nu Z. EX (EZ \cup (Z \land \{b,c\} \newline
Z_0=S \newline
Z_1=EX (EZ_0.\cup(Z_0 \land \{b,c\})) \newline
\rightarrow EX (E\,S\,\cup \{b,c\}) \newline
\rightarrow EX (E\,S\,\cup \{b,c\} = EF \{b,c\}=S)  \newline
\rightarrow EX (E\,true\,\cup \{b,c\}) = EF \{b,c\}=S  \newline
\newline
Z\,EX(S)=S \newline
S_F=S \newline
$

$
K,a \models AF\,AG\,p \newline
A_{c_1}G_p=\neg E_{c_1}F \neg p = \neg E{c_1}F \{ b \} \newline
\newline
\rightarrow E_{b,c}F \{b\}=\nu Z. ( \{b\} \land S_f) \lor EX\,Z
\rightarrow \nu Z. (\{b\}) \lor EX\,Z \newline
\newline
Z_0=\emptyset \newline
Z_1=\{b\} \lor EX \emptyset = \{b\} \newline
Z_2=\{b\} \lor EX \{b\} = \{a,b\} \newline
Z_3=\{b\} \lor EX \{a,b\}=\{a,b\}=Z_2 \newline
$

So, $A_{c_1}Gp={a,b}$

$
K,a \models A_{c_1}F\{a,b\}=\neg E_{c_1}G \neg \{a,b\} = \neg E_{c_1}G \{c\} \newline
\rightarrow E_{b,c}G\{c\}=\nu Z.\{c\} \land EX (E \, Z \, \cup (Z \land \{b,c\}))
\newline
Z_0=S \newline
Z_1=\{c\} \land EX (E \, Z_0 \cup Z_0 \land \{b,c\})) \newline
\rightarrow \{c\} \land EX (E \, S \cup \{b,c\})=\{c\} \land \{EX\,EF\{b,c\} \newline
\rightarrow \{c\} \land EX S = \{c\} \newline
Z_2=\{c\} \land EX(E\,Z_1 \cup (Z_1 \land \{b,c\})) \newline
\rightarrow \{c\} \land EX(E\,\{c\} \cup \{c\})=\{c\}=Z_1  
$

$
\neg E_{b,c}G\{c\}=\{a,b\} \Rightarrow [[A_c\,F\,AG\,p]]_k=\{a,b\}
K,a \models AF\,AG\,p \newline
c_1=\{b,c\}
$

The Kripke structure \textbf{holds}, since we have $[[A_c\,F\,AG\,p]]_k=\{a,b\}$ in which includes the initial path.

\subsection*{Question 03}

Propositions without fairness:

For \emph{mutual exclusion}:
\begin{lstlisting}
AG(!(ph0.self=EATING * ph1.self=EATING));
AG(!(ph1.self=EATING * ph2.self=EATING));
AG(!(ph2.self=EATING * ph3.self=EATING));
AG(!(ph3.self=EATING * ph0.self=EATING));
\end{lstlisting}

For \emph{progress deadlock}:
\begin{lstlisting}
!EF(AG(ph0.self=HUNGRY));
!EF(AG(ph1.self=HUNGRY));
!EF(AG(ph2.self=HUNGRY));
!EF(AG(ph3.self=HUNGRY));
\end{lstlisting}

For \emph{starvation}:
\begin{lstlisting}
!EF(EG(ph0.self=HUNGRY));
!EF(EG(ph1.self=HUNGRY));
!EF(EG(ph2.self=HUNGRY));
!EF(EG(ph3.self=HUNGRY));
\end{lstlisting}

Propositions to add fairness:
\begin{lstlisting}
!(ph0.self=EATING);
!(ph1.self=EATING);
!(ph2.self=EATING);
!(ph3.self=EATING);
\end{lstlisting}

Dining version 2 with fairness, output:
\begin{lstlisting}
# MC: formula passed --- AG(!((ph0.self=EATING * ph1.self=EATING)))
# MC: formula passed --- AG(!((ph1.self=EATING * ph2.self=EATING)))
# MC: formula passed --- AG(!((ph2.self=EATING * ph3.self=EATING)))
# MC: formula passed --- AG(!((ph3.self=EATING * ph0.self=EATING)))
# MC: formula passed --- !(EF(AG(ph0.self=HUNGRY)))
# MC: formula passed --- !(EF(AG(ph1.self=HUNGRY)))
# MC: formula passed --- !(EF(AG(ph2.self=HUNGRY)))
# MC: formula passed --- !(EF(AG(ph3.self=HUNGRY)))
# MC: formula passed --- !(EF(EG(ph0.self=HUNGRY)))
# MC: formula passed --- !(EF(EG(ph1.self=HUNGRY)))
# MC: formula passed --- !(EF(EG(ph2.self=HUNGRY)))
# MC: formula passed --- !(EF(EG(ph3.self=HUNGRY)))
\end{lstlisting}

\section*{Bisimulation, Simulation}

\subsection*{Question 04}

The CTL formula $EX\,AX\,p$ is true for the first Kripke structure, but not
for the second one; therefore they cannot be bisimilar.

\subsection*{Question 05}

\begin{center}
\begin{tabular}{ | l | l || l | l | l | l | l | l | }
  \hline
      A & B &
      \multicolumn{2}{c|}{$t_0$} &
      \multicolumn{2}{c|}{$t_1$} &
      \multicolumn{2}{c|}{$t_2$} \\
  \hline
  \hline
      \multicolumn{2}{|c||}{$s_0$}
      & X & & X & X & X & \\
  \hline
      \multicolumn{2}{|c||}{$s_1$}
      & X & X & X & & X & X \\
  \hline
\end{tabular}
\end{center}

We have initialized both $A$ and $B$ to include all pairs for which:
\[
(s,s') \in S \times S' \textrm{so that}\quad L(s) = L(s')
\]

Which is the pairs $\{(s_0,t_1),(s_1,t_0),(s_1,t_2)\}$. While checking $(s_0,t_0)$ we find that these two properties hold:

\[
\forall (s_0,t) \in T: \exists t' \in S' \quad\textrm{so that}\quad
  (t_0,t') \in T', (t,t') \in B
\]
\[
\forall (t_0,t') \in T': \exists t \in S \quad\textrm{so that}\quad
  (s_0,t) \in T, (t,t') \in B\\
\]

So we mark it as checked in $A$ and leave it as part of $B$. Likewise for
$(s_0,t_2),(s_1,t_1)$. So in conclusion, the two structures are bisimilar
because:

\[
B = \{(s_0,t_0),(s_0,t_2),(s_1,t_1)\}
\]
\[
(s_0,t_0) \in B
\]

Also, bisimilarity implies they are also simulation equivalent.

\subsection*{Question 06}

\lstset{ %
basicstyle=\footnotesize\ttfamily,       % the size of the fonts that are used for the code
%numbers=left,                   % where to put the line-numbers
numberstyle=\footnotesize,      % the size of the fonts that are used for the line-numbers
stepnumber=1,                   % the step between two line-numbers. If it's 1 each line will be numbered
numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
showspaces=false,               % show spaces adding particular underscores
showstringspaces=false,         % underline spaces within strings
showtabs=false,                 % show tabs within strings adding particular underscores
frame=single,			% adds a frame around the code
captionpos=t,			% sets the caption-position to bottom
breaklines=true,		% sets automatic line breaking
breakatwhitespace=false,	% sets if automatic breaks should only happen at whitespace
frameround={t}{f}{f}{f},
}

LTL properties for {\em mutual exclusion}:

\begin{lstlisting}
G(!(ph0.self=EATING * ph1.self=EATING));
G(!(ph1.self=EATING * ph2.self=EATING));
G(!(ph2.self=EATING * ph3.self=EATING));
G(!(ph3.self=EATING * ph0.self=EATING));
\end{lstlisting}

LTL properties for {\em deadlock}:

\begin{lstlisting}
!F(G(ph0.self=HUNGRY * ph1.self=HUNGRY * ph2.self=HUNGRY * ph3.self=HUNGRY));
\end{lstlisting}

LTL properties for {\em starvation}:

\begin{lstlisting}
!F(G(ph0.self=HUNGRY));
!F(G(ph1.self=HUNGRY));
!F(G(ph2.self=HUNGRY));
!F(G(ph3.self=HUNGRY));
\end{lstlisting}

Checking with VIS provides the following results for {\em dining-v1.v},
where we see mutual exclusion is satisfied, however deadlock and starvation are
possible:

\begin{lstlisting}
Formula: G(!((ph0.self=EATING * ph1.self=EATING)))
# LTL_MC: formula passed
Formula: G(!((ph1.self=EATING * ph2.self=EATING)))
# LTL_MC: formula passed
Formula: G(!((ph2.self=EATING * ph3.self=EATING)))
# LTL_MC: formula passed
Formula: G(!((ph3.self=EATING * ph0.self=EATING)))
# LTL_MC: formula passed
Formula: !(F(G((((ph0.self=HUNGRY * ph1.self=HUNGRY) * ph2.self=HUNGRY) * ph3.self=HUNGRY))))
# LTL_MC: formula failed
Formula: !(F(G(ph0.self=HUNGRY)))
# LTL_MC: formula failed
Formula: !(F(G(ph1.self=HUNGRY)))
# LTL_MC: formula failed
Formula: !(F(G(ph2.self=HUNGRY)))
# LTL_MC: formula failed
Formula: !(F(G(ph3.self=HUNGRY)))
# LTL_MC: formula failed
\end{lstlisting}

However for the {\em dining-v2.v} implementation, we see that deadlock is not
possible. However starvation is still a problem:

\begin{lstlisting}
Formula: G(!((ph0.self=EATING * ph1.self=EATING)))
# LTL_MC: formula passed
Formula: G(!((ph1.self=EATING * ph2.self=EATING)))
# LTL_MC: formula passed
Formula: G(!((ph2.self=EATING * ph3.self=EATING)))
# LTL_MC: formula passed
Formula: G(!((ph3.self=EATING * ph0.self=EATING)))
# LTL_MC: formula passed
Formula: !(F(G((((ph0.self=HUNGRY * ph1.self=HUNGRY) * ph2.self=HUNGRY) * ph3.self=HUNGRY))))
# LTL_MC: formula passed
Formula: !(F(G(ph0.self=HUNGRY)))
# LTL_MC: formula failed
Formula: !(F(G(ph1.self=HUNGRY)))
# LTL_MC: formula failed
Formula: !(F(G(ph2.self=HUNGRY)))
# LTL_MC: formula failed
Formula: !(F(G(ph3.self=HUNGRY)))
# LTL_MC: formula failed
\end{lstlisting}

An LTL property that is true for all paths that none of the philosophers will be eating forever:

\begin{lstlisting}
!F(G(ph0.self=EATING) + G(ph1.self=EATING) + G(ph2.self=EATING) + G(ph3.self=EATING));
\end{lstlisting}

We can use that property to construct a new one which checks for starvation.

\begin{lstlisting}
!F(G(ph0.self=EATING) + G(ph1.self=EATING) + G(ph2.self=EATING) + G(ph3.self=EATING)) -> !F(G(ph0.self=HUNGRY));
!F(G(ph0.self=EATING) + G(ph1.self=EATING) + G(ph2.self=EATING) + G(ph3.self=EATING)) -> !F(G(ph1.self=HUNGRY));
!F(G(ph0.self=EATING) + G(ph1.self=EATING) + G(ph2.self=EATING) + G(ph3.self=EATING)) -> !F(G(ph2.self=HUNGRY));
!F(G(ph0.self=EATING) + G(ph1.self=EATING) + G(ph2.self=EATING) + G(ph3.self=EATING)) -> !F(G(ph3.self=HUNGRY));
\end{lstlisting}

Using that property on vis shows that the implementation {\em dining-v2.v} is starvation free:

\begin{lstlisting}
Formula: (!(F((((G(ph0.self=EATING) + G(ph1.self=EATING)) + G(ph2.self=EATING)) + G(ph3.self=EATING)))) -> !(F(G(ph0.self=HUNGRY))))
# LTL_MC: formula passed
Formula: (!(F((((G(ph0.self=EATING) + G(ph1.self=EATING)) + G(ph2.self=EATING)) + G(ph3.self=EATING)))) -> !(F(G(ph1.self=HUNGRY))))
# LTL_MC: formula passed
Formula: (!(F((((G(ph0.self=EATING) + G(ph1.self=EATING)) + G(ph2.self=EATING)) + G(ph3.self=EATING)))) -> !(F(G(ph2.self=HUNGRY))))
# LTL_MC: formula passed
Formula: (!(F((((G(ph0.self=EATING) + G(ph1.self=EATING)) + G(ph2.self=EATING)) + G(ph3.self=EATING)))) -> !(F(G(ph3.self=HUNGRY))))
# LTL_MC: formula passed
\end{lstlisting}

\end{document}
